#!/bin/bash

# 设置环境变量
export LD_LIBRARY_PATH=/home/shadowvm/shadow/klee-change/Release+Asserts/lib:$LD_LIBRARY_PATH

# 定义输出文件
output_file="output.txt"

# 清空输出文件（如果存在）
#> "$output_file"

# 写入固定内容到输出文件
content="Hello, world! This is some text written by a shell script.sadasdasd"
echo "$content" >> "$output_file"
#echo "File '$output_file' has been created with the following content:"
#cat "$output_file"

# 定义程序列表和输入
programs=("divide2" "factorial" "fib" "fib2" "getsign" 
"is_prime2" "odd" "pos" "oneN1"  "LoopUnreach2" 
"LoopUnreach5" "LoopUnreach10" "LoopUnreach15" "LoopUnreach20" "LoopMult2" 
"LoopMult5" "LoopMult10" "LoopMult15" "LoopMult20" "LoopSub"
 "UnchLoop" "FirstV1" "FirstV2" "FirstV3" "FirstV4" 
"FirstV5" "SecondV1" "SecondV2" "SecondV3" "SecondV4" "SecondV5")

inputs=("5 4" "2" "2" "2" "2" 
"6" "6" "6" "9" "" 
"5" "9" "13" "18" "" 
"5" "10" "13" "18" "" 
"" "-1 2" "3 2" "15 2" "63 2" 
"127 2" "1 1" "120 120" "120 120" "130 130" "120 120")

declare -i j=329
# 循环每个程序
for program in "${programs[@]}"; do
    let j++
    echo "$j"
    cd "${programs[j]}"

    # 编译程序
    llvm-gcc -DRESOLVE_KLEE_CHANGE=0 -I/home/shadowvm/shadow/shadow-llvm-tools/include/ -emit-llvm -c neq.c -o neq.bc -std=c99

    total_execution_time=0

    # 循环每个程序执行三次
    for ((i=1; i<=3; i++)); do
        # 记录脚本开始执行的时间
        start_time=$(date +%s.%N)
    
    #
    echo "${programs[j]} ${inputs[j]}"
    klee --posix-runtime --libc=uclibc --zest --shadow --use-shadow-version=product --shadow-allow-allocs=true --emit-all-errors --symbolic-after-divergence=true --max-shadow-symbex-time=570 --max-time=600 --watchdog=true --max-solver-time=30 --search=bfs --shadow-replay-standalone=false --shadow-only-symbolic-tests=false --stop-after-n-tests=10000 --output-source=false --shadow-expr-check-equiv=true --switch-type=simple neq.bc ${inputs[j]} >/dev/null 2>&1

    gcc -L /home/shadowvm/shadow/klee-change/Release+Asserts/lib neq.c -lkleeRuntest -DRESOLVE_KLEE_CHANGE=-1 -o old_version -std=c99
    gcc -L /home/shadowvm/shadow/klee-change/Release+Asserts/lib neq.c -lkleeRuntest -DRESOLVE_KLEE_CHANGE=1 -o new_version -std=c99


    #
    for ktest_file in klee-last/*.ktest; do
        klee-replay ./old_version "$ktest_file" >/dev/null 2>&1
        klee-replay ./new_version "$ktest_file" >/dev/null 2>&1
    done

        # 记录脚本执行完毕的时间
        end_time=$(date +%s.%N)

        # 计算执行时间
        execution_time=$(echo "scale=6; ($end_time - $start_time) / 1" | bc -l)
        echo "${programs[j]} $i执行时间为: $execution_time 秒" >> "$output_file"

        # 累加执行时间
        total_execution_time=$(echo "$total_execution_time + $execution_time" | bc -l)
    done

    # 计算平均执行时间
    average_execution_time=$(echo "scale=6; $total_execution_time / 3" | bc -l)

    # 输出平均执行时间
    echo "${programs[j]} 平均执行时间为: $average_execution_time 秒" >> "$output_file"
    echo "$content" >> "$output_file"

    # 返回上一级目录
    cd ..


    
done >> "$output_file"
    if [ $? -ne 0 ]; then
    echo "脚本执行出错"
    exit 1
    fi

